A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))  (k:Knd. ma-interface-domb(I;i;k)  ) 

latex

Definitions	ma-interface-domb(I;i;k), MaInterface(T), ma-interface-locs(I), t  T, , Knd, x:A. B(x), Id, (x  l), P  Q, Type, b, x. t(x), a:A fp B(a), {x:A| B(x)} , State(ds), Top, left + right, x:AB(x), x:A  B(x), f(x), hasloc(k;i), IdDeq, x.A(x), s = t, P  Q, P & Q, P  Q, Atom$n, a < b, type List, Void, x:A.B(x), x:A. B(x), <a, b>, S  T, , IdLnk, KindDeq, x  dom(f)
Lemmas	Kind-deq wf, fpf-dom wf, IdLnk wf, subtype rel product, subtype rel list, subtype rel function, subtype rel set, l member wf, subtype-set-hasloc, member-fpf-dom, fpf-trivial-subtype-top, Id wf, id-deq wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, fpf-ap wf